disjoint_sublists(T;L1;L2;L)
== f1:{0..||L1||}{0..||L||}
== f2:{0..||L2||}{0..||L||}
== (increasing(f1;||L1||) & (j:{0..||L1||}. L1[j] = L[(f1(j))])
== & increasing(f2;||L2||) & (j:{0..||L2||}. L2[j] = L[(f2(j))])
== & (j1:{0..||L1||}, j2:{0..||L2||}. (f1(j1) = f2(j2)))) 

latex

---

clarification:

disjoint_sublists(T;L1;L2;L)
== f1:{0..||L1||}{0..||L||}
== f2:{0..||L2||}{0..||L||}
== (increasing(f1;||L1||) & (j:{0..||L1||}. L1[j] = L[(f1(j))]  T)
== & increasing(f2;||L2||) & (j:{0..||L2||}. L2[j] = L[(f2(j))]  T)
== & (j1:{0..||L1||}, j2:{0..||L2||}. (f1(j1) = f2(j2)  ))) 

latex

Definitions	x:A. B(x), x:AB(x), P & Q, increasing(f;k), l[i], x:A. B(x), {i..j}, #$n, ||as||, A, s = t, , f(a)
FDL editor aliases	disjoint_sublists